\begin{tabbing}
ecl{-}halt(${\it ds}$; ${\it da}$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$n$,$L$. ($n$ = 0)
\\[0ex]$\wedge$ ($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex]$\exists$\=$s$:decl{-}state(${\it ds}$)\+
\\[0ex]$\exists$\=$v$:ma{-}valtype(${\it da}$; $k$)\+
\\[0ex]((($L$ = append(${\it L'}$; cons($<$$k$, $s$, $v$$>$; []))) $\wedge$ ($\uparrow$(${\it test}$($s$,$v$))))
\\[0ex]$\wedge$ l\_all(\=${\it L'}$;\+
\\[0ex]event{-}info(${\it ds}$;${\it da}$);
\\[0ex]$t$.($\neg$spreadn($t$; ${\it k'}$,$s$,$v$.(($k$ = ${\it k'}$) c$\wedge$ ($\uparrow$(${\it test}$($s$,$v$))))))))));
\-\-\-\-\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$L$. ((0 $<$ $n$) $\wedge$ (${\it ha}$($n$,$L$)))
\\[0ex]$\vee$ ($\exists$\=$L_{1}$,$L_{2}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](($L$ = append($L_{1}$; $L_{2}$)) $\wedge$ (${\it ha}$(0,$L_{1}$)) $\wedge$ (${\it hb}$($n$,$L_{2}$)))));
\-\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$L$. (($n$ = 0)
\\[0ex]$\Rightarrow$ \=(((${\it ha}$(0,$L$))\+
\\[0ex]$\wedge$ ($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\wedge$ (${\it hb}$(0,${\it L'}$)))))
\-\\[0ex]$\vee$ \=((${\it hb}$(0,$L$))\+
\\[0ex]$\wedge$ ($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\wedge$ (${\it ha}$(0,${\it L'}$)))))))
\-\-\-\\[0ex]$\wedge$ \=((0 $<$ $n$)\+
\\[0ex]$\Rightarrow$ \=(((${\it ha}$($n$,$L$))\+
\\[0ex]$\wedge$ \=($\forall$$m$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (${\it hb}$($m$,${\it L'}$)) $\Rightarrow$ ((${\it L'}$ = $L$) $\wedge$ ($n$ $\leq$ $m$))))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$L$))\+
\\[0ex]$\wedge$ \=($\forall$$m$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ (${\it ha}$($m$,${\it L'}$))
\\[0ex]$\Rightarrow$ ((${\it L'}$ = $L$) $\wedge$ ($n$ $\leq$ $m$)))))));
\-\-\-\-\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$L$. ((${\it ha}$($n$,$L$))
\\[0ex]$\wedge$ \=($\forall$$m$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (${\it hb}$($m$,${\it L'}$)) $\Rightarrow$ ((${\it L'}$ = $L$) $\wedge$ ($n$ $\leq$ $m$))))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$L$))\+
\\[0ex]$\wedge$ \=($\forall$$m$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (${\it ha}$($m$,${\it L'}$)) $\Rightarrow$ ((${\it L'}$ = $L$) $\wedge$ ($n$ $\leq$ $m$)))));
\-\-\\[0ex]$a$,${\it ha}$.($\lambda$$n$,$L$. (0 $<$ $n$) $\wedge$ (star{-}append(event{-}info(${\it ds}$;${\it da}$); (${\it ha}$(0)); (${\it ha}$($n$)))($L$)));
\\[0ex]$a$,$m$,${\it ha}$.${\it ha}$;
\\[0ex]$a$,$m$,${\it ha}$.($\lambda$$n$,$L$. ((0 $<$ $n$) $\wedge$ (${\it ha}$($n$,$L$))) $\vee$ (($n$ = $m$) $\wedge$ (${\it ha}$(0,$L$))));
\\[0ex]$a$,$l$,${\it ha}$.($\lambda$$n$,$L$. ((${\it ha}$($n$,$L$)) $\wedge$ ($\neg$($n$ $\in$ $l$)))
\\[0ex]$\vee$ (($n$ = 0) $\wedge$ l\_exists($l$; $\mathbb{N}$; $m$.(${\it ha}$($m$,$L$))))))
\-
\end{tabbing}